Inference at * 1 1 2 1 1 
Iof proof for Lemma list extensionality:



1. T : Type
2. T List
3. u : T
4. v : T List
5. b:(T List). (||v|| = ||b||)  (i:. (i < ||v||)  (v[i] = b[i]))  (v = b)
6. T List
7. u1 : T
8. v1 : T List
9. (||[u / v]|| = ||v1||)  (i:. (i < ||[u / v]||)  ([u / v][i] = v1[i]))  ([u / v] = v1)
10. ||v||+1 = ||v1||+1
11. i:. (i < (||v||+1))  ([u / v][i] = [u1 / v1][i])
12. i : 
13. i < ||v||
14. [u / v][(i+1)] = [u1 / v1][(i+1)]
  v[i] = v1[i] 

latex

 by InteriorProof ((((((RWW "select_cons_tl" (-1)) 
CollapseTHENA ((Auto_aux (first_nat 1:n
CollapseTHENA ((Au) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 

CollapseTHENA ((Au)CollapseTHEN (ArithSimp (-1)))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
CollapseTHEN ((Aut) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	P  Q, P  Q, , True, T, False, A, P & Q, A  B, t  T, P  Q, , x:A. B(x)
Lemmas	select cons tl, le wf, squash wf, select wf, length wf1